{\rtf1\ansi\ansicpg1252\uc1\deff0
{\fonttbl{\f0\fmodern\fcharset0\fprq2 RobotoMono-SemiBold;}}
{\colortbl;\red0\green0\blue0;\red255\green255\blue255;\red128\green128\blue128;}
\paperw12240\paperh15840\margl1800\margr1800\margt1440\margb1440\f0\fs22\cf0
\pard\plain \tx0\tx360\tx720\tx1080\tx1440\tx1800\tx2160\tx2880\tx3600\tx4320\ltrch\loch {\f0\fs22\b0\i0 Even though TLA+ isn\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92t executable, there\u8217\'92s a very simple model of computation at the core of Lamport's temporal logic that\u8217\'92s worth digging into - TLA+ models move through time in discrete steps by computing new state from old state. In the paper Lamport calls these steps \u8220\'93actions\u8221\'94: \u8220\'93An action represents a relation between old states and new states, where the unprimed variables refer to the old state and the primed variables refer to the new state\u8221\'94. Paraphrased, \u8220\'93actions\u8221\'94 are not functions that return a value, they\u8217\'92re boolean expressions that define whether or not you can "get from" state A to state B, so to speak.}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 This will be clearer with an example. The Collatz conjecture is an unsolved problem in mathematics that can be defined like this:}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 1. Pick an integer x.}
\par\plain {\f0\fs22\b0\i0 2. If x is is even, set x to x/2.}
\par\plain {\f0\fs22\b0\i0 3. If x is odd, set x to 3*x + 1.}
\par\plain {\f0\fs22\b0\i0 4. If x is not equal to 1, go to step 2.}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 For example, if we start with x = 12 we get the sequence of x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92s = \{ 12, 6, 3, 10, 5, 16, 8, 4, 2, 1 \}. The Collatz conjecture asks if these steps terminate for all positive integers, which is currently unknown but has been checked up to x=2^68.}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 If we want to represent this process using something akin to TLA+ actions, we need some boolean expressions of x and x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92 such that one evaluates to true if x and x\u8217\'92 are adjacent in the Collatz sequence. That turns out to be fairly straightforward:}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 \tab Action A: (x % 2 == 0) && (x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92 == x / 2)}
\par\plain {\f0\fs22\b0\i0 \tab Action B: (x % 2 == 1) && (x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92 == 3 * x + 1)}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 Given these actions, we can \loch\af0\hich\af0\dbch\af0\uc1\u8220\'93get from\u8221\'94 x=10 to x=5 because the pair (x=10, x\u8217\'92=5) makes action A true, and we can \u8220\'93get from\u8221\'94 x=5 to x=16 because the pair (x=5, x\u8217\'92=16) makes action B true. The pair (x=17, x\u8217\'92=1) satisfies neither action, so it can\u8217\'92t be in the sequence. To \u8220\'93run\u8221\'94 these actions for some arbitrary starting value of x we first find a value of x\u8217\'92 that makes one of our actions true, then replace x with x\u8217\'92 and repeat.}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 Now for something slightly brain-hurty. If we swap x and x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92 in our actions, we get the same state relations except with the time axis reversed. We can run the system \u8220\'93backwards\u8221\'94 - we can always get from x to x*2 via backward-action-A, and we can get from x to (x-1)/3 if (x-1)/3 is an odd integer via backward-action-B. We can also refactor our expressions to keep our swapped actions in the same form as earlier:}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 \tab Backward Action A: (x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92 == x * 2)}
\par\plain {\f0\fs22\b0\i0 \tab Backward Action B: (x % 6 == 4) && (x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92 == (x - 1) / 3)}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 Take a moment to plug in some values of x and x\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92 until you\u8217\'92re convinced that these actions accept the same pairs as the earlier ones, just with the values swapped. There\u8217\'92s a key difference here though - if we want to \u8220\'93run\u8221\'94 the reversed program starting with x = 10, we hit a problem - both (x=10, x\u8217\'92=20) and (x=10, x\u8217\'92=3) make an action true, so which x\u8217\'92 do we choose as our \u8220\'93new\u8221\'94 x? In this case, the answer is \u8220\'93both\u8221\'94 - because this is a _specification_ and not a _program_. If we draw an arrow between x and x\u8217\'92 for all valid pairs, we get a graph where all values lead to 1 in \u8220\'93forward\u8221\'94 mode and 1 leads to all values in \u8220\'93backward\u8221\'94 mode. It might not initially seem reasonable to have a program with multiple possible \u8220\'93future\u8221\'94 states, but it\u8217\'92s perfectly well defined - we\u8217\'92re just used to programs changing state in response to inputs, of which there aren\u8217\'92t any here.}
\par\plain \f0\fs22\b0\i0
\par\plain {\field{\*\fldinst HYPERLINK "https://xkcd.com/710"}{\fldrslt\f0\fs22\b0\i0 https://xkcd.com/710}}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 **something from the tla paper here**}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 So how can we summarize the computational model that TLA+ uses?}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 1. A program is a blob of state. There is no implicit state - no stacks, no registers, no threads.}
\par\plain {\f0\fs22\b0\i0 2. Programs \loch\af0\hich\af0\dbch\af0\uc1\u8220\'93run\u8221\'94 by atomically transitioning between states. Partially-modified states are never externally visible.}
\par\plain {\f0\fs22\b0\i0 3. Transitions between states are pure functions that compute \loch\af0\hich\af0\dbch\af0\uc1\u8220\'93new\u8221\'94 states from \u8220\'93old\u8221\'94 states without side effects.}
\par\plain {\f0\fs22\b0\i0 4. The set of all possible states combined with all possible transitions forms a directed graph.}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 This is roughly equivalent to a \loch\af0\hich\af0\dbch\af0\uc1\u8220\'93nondeterministic finite automaton\u8221\'94 or a Mealy machine, with looser restrictions -  we don\u8217\'92t care about sets of symbols or stopping conditions or if the states or symbols are finite, }
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 *******TRANSITION SYSTEMS********}
\par\plain \f0\fs22\b0\i0
\par\pard\plain \ltrch\loch {\field{\*\fldinst HYPERLINK "https://en.wikipedia.org/wiki/Category:Models_of_computation"}{\fldrslt\f0\fs22 https://en.wikipedia.org/wiki/Category:Models_of_computation}}
\par\pard\plain \tx0\tx360\tx720\tx1080\tx1440\tx1800\tx2160\tx2880\tx3600\tx4320\ltrch\loch \f0\fs22\b0\i0
\par\pard\plain \ltrch\loch {\field{\*\fldinst HYPERLINK "https://en.wikipedia.org/wiki/Abstract_machine"}{\fldrslt\f0\fs22 https://en.wikipedia.org/wiki/Abstract_machine}}
\par\plain \f0\fs22
\par\plain {\field{\*\fldinst HYPERLINK "https://en.wikipedia.org/wiki/Automata_theory"}{\fldrslt\f0\fs22 https://en.wikipedia.org/wiki/Automata_theory}}
\par\plain \f0\fs22
\par\plain {\field{\*\fldinst HYPERLINK "https://en.wikipedia.org/wiki/Well-structured_transition_system"}{\fldrslt\f0\fs22 https://en.wikipedia.org/wiki/Well-structured_transition_system}}
\par\plain \f0\fs22
\par\plain {\field{\*\fldinst HYPERLINK "https://en.wikipedia.org/wiki/Synchronous_circuit"}{\fldrslt\f0\fs22 https://en.wikipedia.org/wiki/Synchronous_circuit}}
\par\plain \f0\fs22
\par\plain {\field{\*\fldinst HYPERLINK "https://en.wikipedia.org/wiki/Mealy_machine"}{\fldrslt\f0\fs22 https://en.wikipedia.org/wiki/Mealy_machine}}
\par\plain \f0\fs22
\par\plain {\field{\*\fldinst HYPERLINK "https://en.wikipedia.org/wiki/Sequential_logic"}{\fldrslt\f0\fs22 https://en.wikipedia.org/wiki/Sequential_logic}}
\par\plain \f0\fs22
\par\plain 
\par\plain 
\par\pard\plain \tx0\tx360\tx720\tx1080\tx1440\tx1800\tx2160\tx2880\tx3600\tx4320\ltrch\loch {\f0\fs22\b0\i0 Something something}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 Let\loch\af0\hich\af0\dbch\af0\uc1\u8217\'92s look at the same system expressed as an imperative program and a temporal program:}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 **imperative uart**}
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 **temporal uart**}
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 \line "Applicative State Transition" doesn't even appear in Wikipedia!!!}
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain {\f0\fs22\b0\i0 We can state that a bit more formally as the simple recurrence "x' = f(x)", where "x" represents the _old_ state of the program, "x'" represents the _new_ state of the program, and "f" is a pure function that computes the entire new state from the old state. If we add an input and output we get "(x, o)' = f(x, i)", which is roughly equivalent to a Mealy machine except that our states and in/outputs are arbitrary data structures instead of sets of states and symbols.}
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0
\par\plain \f0\fs22\b0\i0}